(declare-fun a () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun d () Real)
(declare-fun e () Real)
(assert (<= (+ (ite c 1 0) (ite b 1 0)) 1))
(assert (= (ite c 1 0) (ite (>= (+ (ite b 1 0) (ite a (- 1) 0)) 1) 1 0)))
(assert (<= d 0 (+ (ite b 1 0) (ite a 1 0)) e))
(check-sat)
